package discretePso;


import java.io.*;

public class SATInstance {
	public int numVariables;
	public int numClauses;
	public int[][] clauses;
	
	public SATInstance(File file){
		char[] fileArray = new char[(int)file.length()];
		try{
			FileReader reader = new FileReader(file);
			reader.read(fileArray, 0, (int)file.length());
		}catch(Exception e){
			e.printStackTrace();
		}
		String fileString = String.valueOf(fileArray);
		int ind = fileString.indexOf("p cnf") + 6;
		fileString = fileString.substring(ind);
		String[] fileStringArray = fileString.split("\\n"); 
		String[] sArray = fileStringArray[0].split("\\s");
		numVariables = Integer.parseInt(sArray[0]);
		numClauses = Integer.parseInt(sArray[1]);
		
		clauses = new int[numClauses][3];
		for(int i = 0; i < numClauses; i++){
			sArray = fileStringArray[i+1].split("\\s");
			for(int j = 0; j < 3; j++){
				clauses[i][j] = Integer.parseInt(sArray[j]);
			}
			
		}
	}
	
	/*
	 * Returns the number of satisfied clauses for a given truth-value assignment.
	 * An assignment is a vector of boolean values of length the number 
	 * of variables in the instance (numVars).
	 */
	public int evaluate(boolean[] assignment){
		int numTrueClauses = 0;
		for(int i = 0; i < numClauses; i++){
			if(	(	(clauses[i][0] > 0 	&& 	assignment[	clauses[i][0] - 1]) || 
					(clauses[i][0] <= 0 && !assignment[-clauses[i][0] - 1])) ||
				(	(clauses[i][1] > 0 	&& 	assignment[	clauses[i][1] - 1]) || 
					(clauses[i][1] <= 0 && !assignment[-clauses[i][1] - 1])) ||
				(	(clauses[i][2] > 0 	&& 	assignment[	clauses[i][2] - 1]) || 
					(clauses[i][2] <= 0 && !assignment[-clauses[i][2] - 1])))
				numTrueClauses++;
		}
		return numTrueClauses;
	}
	
	
}
